A:Type, as:(A List), n:int_iseg(0; ||as||). ||firstn(n; as)|| = n   

latex

Definitions	t  T, x:A. B(x), T, ff, P  Q, P  Q, P  Q, tt, P  Q, if b then t else f fi , Y, firstn(n; as), ||as||, True, prop{i:l}, Unit, , int_iseg(i; j), False, A, A  B,
Lemmas	length wf1, length wf2, int iseg wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, assert of lt int, eqtt to assert, iff transitivity, bnot wf, le wf, le int wf, assert wf, bool wf, lt int wf, add functionality wrt eq, length cons, non neg length, firstn wf